Crate contracts

A crate implementing "Design by Contract" via procedural macros.

This crate is heavily inspired by the libhoare compiler plugin.

The main use of this crate is to annotate functions and methods using "contracts" in the form of pre-conditions, post-conditions and invariants.

Each "contract" annotation that is violated will cause an assertion failure.

The attributes use "function call form" and can contain 1 or more conditions to check. If the last argument to an attribute is a string constant it will be inserted into the assertion message.

Example

#[pre(x > 0, "x must be in the valid input range")]
#[post(ret.is_some() ==> ret.unwrap() * ret.unwrap() == x)]
fn integer_sqrt(x: u64) -> Option<u64> {
   // ...
}

pub struct Library {
    available: HashSet<String>,
    lent: HashSet<String>,
}

impl Library {
    fn book_exists(&self, book_id: &str) -> bool {
        self.available.contains(book_id)
            || self.lent.contains(book_id)
    }

    #[debug_pre(!self.book_exists(book_id), "Book IDs are unique")]
    #[debug_post(self.available.contains(book_id), "Book now available")]
    #[post(self.available.len() == old(self.available.len()) + 1)]
    #[post(self.lent.len() == old(self.lent.len()), "No lent change")]
    pub fn add_book(&mut self, book_id: &str) {
        self.available.insert(book_id.to_string());
    }

    #[debug_pre(self.book_exists(book_id))]
    #[post(ret ==> self.available.len() == old(self.available.len()) - 1)]
    #[post(ret ==> self.lent.len() == old(self.lent.len()) + 1)]
    #[debug_post(ret ==> self.lent.contains(book_id))]
    #[debug_post(!ret ==> self.lent.contains(book_id), "Book already lent")]
    pub fn lend(&mut self, book_id: &str) -> bool {
        if self.available.contains(book_id) {
            self.available.remove(book_id);
            self.lent.insert(book_id.to_string());
            true
        } else {
            false
        }
    }

    #[debug_pre(self.lent.contains(book_id), "Can't return a non-lent book")]
    #[post(self.lent.len() == old(self.lent.len()) - 1)]
    #[post(self.available.len() == old(self.available.len()) + 1)]
    #[debug_post(!self.lent.contains(book_id))]
    #[debug_post(self.available.contains(book_id), "Book available again")]
    pub fn return_book(&mut self, book_id: &str) {
        self.lent.remove(book_id);
        self.available.insert(book_id.to_string());
    }
}

Attributes

This crate exposes the pre, post and invariant attributes.

• pre-conditions are checked before a function/method is executed.
• post-conditions are checked after a function/method ran to completion
• invariants are checked both before and after a function/method ran.

Additionally, all those attributes have versions with different "modes". See [the Modes section][#Modes] below.

For traits and trait impls the contract_trait attribute can be used.

Pseudo-functions and operators

old() function

One unique feature that this crate provides is an old() pseudo-function which allows to perform checks using a value of a parameter before the function call happened. This is only available in post attributes.

#[post(*x == old(*x) + 1, "after the call `x` was incremented")]
fn incr(x: &mut usize) {
    *x += 1;
}

==> operator

For more complex functions it can be useful to express behaviour using logical implication. Because Rust does not feature an operator for implication, this crate adds this operator for use in attributes.

#[post(person_name.is_some() ==> ret.contains(person_name.unwrap()))]
fn geeting(person_name: Option<&str>) -> String {
    let mut s = String::from("Hello");
    if let Some(name) = person_name {
        s.push(' ');
        s.push_str(name);
    }
    s.push('!');
    s
}

This operator is right-associative.

Note: Because of the design of syn, it is tricky to add custom operators to be parsed, so this crate performs a rewrite of the TokenStream instead. The rewrite works by separating the expression into a part that's left of the ==> operator and the rest on the right side. This means that if a ==> b { c } else { d } will not generate the expected code. Explicit grouping using parenthesis or curly-brackets can be used to avoid this.

Feature flags

Following feature flags are available:

• disable_contracts - disables all checks and assertions.
• override_debug - changes all contracts (except test_ ones) into debug_* versions
• override_log - changes all contracts (except test_ ones) into a log::error!() call if the condition is violated. No abortion happens.
• mirai_assertions - instead of regular assert! style macros, emit macros used by the MIRAI static analyzer.

Attribute Macros

contract_trait	A "contract_trait" is a trait which ensures all implementors respect all provided contracts.
debug_invariant	Same as invariant, but uses debug_assert!.
debug_post	Same as post, but uses debug_assert!.
debug_pre	Same as pre, but uses debug_assert!.
invariant	Invariants are conditions that have to be maintained at the "interface boundaries".
post	Post-conditions are checked after the function body is run.
pre	Pre-conditions are checked before the function body is run.
test_invariant	Same as invariant, but is only enabled in #[cfg(test)] environments.
test_post	Same as post, but is only enabled in #[cfg(test)] environments.
test_pre	Same as pre, but is only enabled in #[cfg(test)] environments.